$\forall$$T$:Type, $P$:($T$$\rightarrow\mathbb{P}$), $L$:($T$ List).
\\[0ex](0 $<$ $\parallel$$L$$\parallel$)
\\[0ex]$\Rightarrow$ ($\forall$$x$, $y$:$T$. Dec($x$ = $y$))
\\[0ex]$\Rightarrow$ (($\forall$$x$$\in$$L$. $\forall$$y$$\in$$L$. ($\neg$($x$ = $y$ $\in$ $T$)) $\Rightarrow$ ($P$($x$) $\vee$ $P$($y$))) $\Leftarrow\!\Rightarrow$ ($\exists$$x$$\in$$L$.$\forall$$y$$\in$$L$. ($\neg$($x$ = $y$ $\in$ $T$)) $\Rightarrow$ $P$($y$)))